Problem: f(n__f(n__a())) -> f(n__g(n__f(n__a()))) f(X) -> n__f(X) a() -> n__a() g(X) -> n__g(X) activate(n__f(X)) -> f(X) activate(n__a()) -> a() activate(n__g(X)) -> g(activate(X)) activate(X) -> X Proof: Bounds Processor: bound: 2 enrichment: match automaton: final states: {7,6,5,4} transitions: g1(55) -> 56* activate1(62) -> 63* activate1(64) -> 65* activate1(54) -> 55* a1() -> 53* f1(40) -> 41* f1(10) -> 11* f1(46) -> 47* f1(48) -> 49* n__g1(30) -> 31* n__g1(32) -> 33* n__g1(9) -> 10* n__g1(38) -> 39* n__a1() -> 8* n__f1(20) -> 21* n__f1(26) -> 27* n__f1(18) -> 19* n__f1(8) -> 9* n__g2(86) -> 87* f0(2) -> 4* f0(1) -> 4* f0(3) -> 4* n__a2() -> 84* n__f0(2) -> 1* n__f0(1) -> 1* n__f0(3) -> 1* n__f2(82) -> 83* n__f2(74) -> 75* n__f2(76) -> 77* n__f2(68) -> 69* n__a0() -> 2* n__g0(2) -> 3* n__g0(1) -> 3* n__g0(3) -> 3* a0() -> 5* g0(2) -> 6* g0(1) -> 6* g0(3) -> 6* activate0(2) -> 7* activate0(1) -> 7* activate0(3) -> 7* 1 -> 7,62,46,32,20 2 -> 7,54,40,38,26 3 -> 7,64,48,30,18 8 -> 5* 10 -> 68* 11 -> 47,7,4 19 -> 4* 21 -> 4* 27 -> 4* 31 -> 6* 33 -> 6* 39 -> 6* 40 -> 82* 41 -> 63,55,7 46 -> 74* 47 -> 63,55,7 48 -> 76* 49 -> 63,55,7 53 -> 55,7 54 -> 55* 55 -> 86* 56 -> 65,55,7 62 -> 63,55 63 -> 55* 64 -> 65* 65 -> 55* 69 -> 11* 75 -> 47* 77 -> 49,7 83 -> 41,7 84 -> 53,7 87 -> 56,7 problem: Qed